(* Copyright (c) 2009-2012 Tjark Weber. All rights reserved. *)

(* Definition of SMT solvers *)

structure SolverSpec = struct

  datatype result = SAT of string option  (* model, should perhaps be a thm *)
                  | UNSAT of Thm.thm option  (* assumptions |- conclusion *)
                  | UNKNOWN of string option  (* reason for failure *)

  (* calls 'pre' (which is supposed to translate a HOL goal into a list of
     strings that the SMT solver will understand); writes these strings into a
     file; appends the names of input and output files to 'cmd_stem' before
     executing it as a system command; calls 'post' (which is supposed to parse
     the output file generated by the SMT solver); deletes input and output
     file (unless '!trace' = 4); emits messages according to '!trace' *)
  fun make_solver (pre : Abbrev.goal -> 'a * string list)
                  (cmd_stem : string)
                  (post : 'a -> string -> result) : Abbrev.goal -> result =
  fn goal =>
  let
    (* call 'pre goal' to generate SMT solver input *)
    val (x, inputs) = pre goal
    val infile = FileSys.tmpName ()
    val outfile = FileSys.tmpName ()
    fun work() = let
      val _ = Library.write_strings_to_file infile inputs
      val cmd = cmd_stem ^ infile ^ " > " ^ outfile
      (* the actual system call to the SMT solver *)
      val _ = if !Library.trace > 1 then
                Feedback.HOL_MESG ("HolSmtLib: calling external command '" ^
                                   cmd ^ "'")
              else ()
      val _ = Systeml.system_ps cmd
      (* call 'post' to determine the result *)
      val result = post x outfile
      val _ =
          if !Library.trace > 1 then
            Feedback.HOL_MESG(
              "HolSmtLib: solver reports negated term to be '" ^
              (case result of
                   SAT NONE => "satisfiable' (no model given)"
                 | SAT (SOME _) => "satisfiable' (model given)"
                 | UNSAT NONE => "unsatisfiable' (no proof given)"
                 | UNSAT (SOME thm) =>
                   if !Library.trace > 2 then
                     "unsatisfiable' (theorem: " ^Hol_pp.thm_to_string thm ^ ")"
                   else
                     "unsatisfiable' (proof checked)"
                 | UNKNOWN NONE => "unknown' (no reason given)"
                 | UNKNOWN (SOME _) => "unknown' (reason given)"))
          else ()
      (* if the SMT solver returned a theorem 'thm', then this should be of the
         form "A' |- g" with A' \subseteq A, where (A, g) is the input goal *)
      val _ = if !Library.trace > 0 then
                case result of
                    UNSAT (SOME thm) =>
                    let
                      val (As, g) = goal
                      val As = HOLset.fromList Term.compare As
                    in
                      if not (HOLset.isSubset (Thm.hypset thm, As)) then
                        Feedback.HOL_WARNING "SolverSpec" "make_solver"
                                    "theorem contains additional hyp(s)"
                      else ();
                      if not (Term.aconv (Thm.concl thm) g) then
                        Feedback.HOL_WARNING "SolverSpec" "make_solver"
                             "conclusion of theorem does not match goal"
                      else ()
                    end
                  | _ => ()
              else ()
    in
      result
    end
    fun finish () =
        (* delete all temporary files *)
        if !Library.trace < 4 then
          List.app (fn path => OS.FileSys.remove path handle SysErr _ => ())
                   [infile, outfile]
        else ()
  in
    Portable.finally finish work ()
  end

  (* simplifies the goal to eliminate (some) terms that are not supported by
     the respective SMT solver; simp_tac must produce at most one subgoal *)
  fun simplify simp_tac goal =
  let
    val (new_goal, validation) = case simp_tac goal of
        ([], validation) =>
        (* apply the SMT solver anyway, but to the trivial goal ``T`` *)
        (([], boolSyntax.T), fn _ => validation [])
      | ([new_goal], validation) =>
        (new_goal, validation)
      | _ =>
        raise Feedback.mk_HOL_ERR "SolverSpec" "simplify"
          "simplification produced more than one subgoal"
  in
    if !Library.trace > 2 then
      let
        fun goal_to_string (asl, g) =
          "[" ^ String.concatWith ", " (List.map Hol_pp.term_to_string asl) ^
            "] |- " ^ Hol_pp.term_to_string g
      in
        Feedback.HOL_MESG
          ("HolSmtLib: simplified goal is " ^ goal_to_string new_goal)
      end
    else ();
    (new_goal, validation)
  end

end
